/*********************************************************************
Author: Simone Fulvio Rollini <simone.rollini@gmail.com>

Periplo -- Copyright (C) 2013, Simone Fulvio Rollini

Periplo is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

Periplo is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with Periplo. If not, see <http://www.gnu.org/licenses/>.
 *********************************************************************/

#ifdef PRODUCE_PROOF
#include "PG.h"

using namespace periplo;

/************************* HELPERS ******************************/

bool ProofGraph::decideOnAlternativeInterpolation(ProofNode* n)
{
	// Get antecedents partial interpolants
	Enode * I1 = n->getAnt1()->getPartialInterpolant();
	Enode * I2 = n->getAnt2()->getPartialInterpolant();
	assert( I1 ); assert( I2 );
	bool I1_is_true = ( I1 == egraph.mkTrue() );
	bool I2_is_true = ( I2 == egraph.mkTrue() );
	bool I1_is_false = ( I1 == egraph.mkFalse() );
	bool I2_is_false = ( I2 == egraph.mkFalse() );
	bool I1_is_none = ( !I1_is_true && !I1_is_false );
	bool I2_is_none = ( !I2_is_true && !I2_is_false );

	// For some combinations of I1, I2, the alternative interpolant
	// has a smaller size!
	// Standard     (I1 \/ p ) /\ (I2 \/ ~p)
	// Alternative  (I1 /\ ~p) \/ (I2 /\ p)

	if(I1_is_false && I2_is_none) return true;
	if(I1_is_none && I2_is_false) return true;
	if(I1_is_false && I2_is_false) return true;
	return false;
}

#ifdef FULL_LABELING
void ProofGraph::computeABVariablesMapping( const ipartitions_t & A_mask )
{
	// Track AB class variables and associate index to them
	// NOTE class A has value -1, class B value -2, undetermined value -3, class AB has index bit from 0 onwards
	int AB_bit_index = 0;
	for( std::set<Var>::iterator nv = proof_variables.begin(); nv != proof_variables.end(); nv++ )
	{
		Var v = (*nv);
		icolor_t v_class = getVarClass( v, A_mask );
		if( v_class == I_A ){ AB_vars_mapping[v] = -1; }
		else if( v_class == I_B ){ AB_vars_mapping[v] = -2; }
		else if( v_class == I_AB ){ AB_vars_mapping[v] = AB_bit_index; AB_bit_index++; }
		else periplo_error_();
	}
}

// Input: node, current interpolant partition masks for A and B
// e.g. 0---010 first partition in A
// node
// Output: returns node pivot color as a, b or ab
// depending on the colors in the node antecedents
icolor_t ProofGraph::getPivotColor( ProofNode* n )
{
	assert( !n->isLeaf() );
	Var v = n->getPivot();
	// In labeling, classes and colors are distinct
	icolor_t var_class = getVarClass2( v );

	// Update AB vars color vectors from antecedents
	updateColoringfromAnts(n);

	icolor_t var_color = I_UNDEF;
	// Determine if variable A-local, B-local or AB-common
	if ( var_class == I_A || var_class == I_B ) var_color = var_class;
	else if (  var_class == I_AB )
	{
		if( isColoredA( n,v ) ) var_color = I_A;
		else if ( isColoredB( n,v )  ) var_color = I_B;
		else if ( isColoredAB( n,v ) ) var_color = I_AB;
		else
		{
			icolor_t var_color_1=I_UNDEF;
			if( isColoredA( n,v ) ) var_color_1 = I_A;
			else if ( isColoredB( n,v )  ) var_color_1 = I_B;
			else if ( isColoredAB( n,v ) ) var_color_1 = I_AB;

			icolor_t var_color_2=I_UNDEF;
			if( isColoredA( n,v ) ) var_color_2 = I_A;
			else if ( isColoredB( n,v )  ) var_color_2 = I_B;
			else if ( isColoredAB( n,v ) ) var_color_2 = I_AB;

			cerr << "Pivot " << v << " has colors " << var_color_1 << " " << var_color_2 <<
					" in antecedents but no color in resolvent" << endl;
			periplo_error_();
		}

		// Remove pivot from resolvent if class AB
		updateColoringAfterRes(n);
	}
	else periplo_error( "Pivot " << v << " has no class" );

	return var_color;
}
#endif

// Input: variable, current interpolant partition masks for A and B
// e.g. 0---010 first partition in A
// Output: returns A-local , B-local or AB-common
icolor_t ProofGraph::getVarClass( Var v, const ipartitions_t & A_mask )
{
	// Get enode corresponding to variable
	Enode * enode_var = thandler->varToEnode( v );

	// TODO look at isAB methods in egraph
	//Determine mask corresponding to B
	ipartitions_t B_mask = ~A_mask;
	//Reset bit 0 to 0
	clrbit( B_mask, 0 );

	//Get partition mask variable
	//e.g. 0---0110 variable in first and second partition
	const ipartitions_t & enode_mask = enode_var->getIPartitions( );

	// Check if variable present in A or B
	const bool var_in_A = ( (enode_mask & A_mask) != 0 );
	const bool var_in_B = ( (enode_mask & B_mask) != 0 );
	assert( var_in_A || var_in_B );

	icolor_t var_class;
	// Determine if variable A-local, B-local or AB-common
	if ( var_in_A && !var_in_B ) var_class = I_A;
	else if ( !var_in_A && var_in_B ) var_class = I_B;
	else if (  var_in_A && var_in_B ) var_class = I_AB;
	else periplo_error( "Variable has no class" );

	return var_class;
}

// Input: proof node, current interpolant partition masks for A and B
// e.g. 0---010 first partition in A
// Output: returns A or B
icolor_t ProofGraph::getClauseColor( const ipartitions_t & clause_mask, const ipartitions_t & A_mask )
{
	// Get partition mask clause
	// e.g. 0---0110 variable in first and second partition

	// TODO look at isAB methods in egraph
	//Determine mask corresponding to B
	ipartitions_t B_mask = ~A_mask;
	//Reset bit 0 to 0
	clrbit( B_mask, 0 );

	// Check if belongs to A or B
	const bool clause_in_A = ( (clause_mask & A_mask) != 0 );
	const bool clause_in_B = ( (clause_mask & B_mask) != 0 );
	assert( clause_in_A || clause_in_B );

	icolor_t clause_color = I_A;

	// Determine if clause belongs to A or B
	if( clause_in_A && !clause_in_B ) clause_color = I_A;
	else if( !clause_in_A && clause_in_B ) clause_color = I_B;
	else if( clause_in_A && clause_in_B ) clause_color = I_AB;
	else periplo_error( "Clause has no color" );

	return clause_color;
}




#endif
